Inference at * 1 
Iof proof for Lemma int sq:



1. x : 
2. y : 
3. x = y
  x ~ y 

latex

 by With  SqEqual 

latex

 1: 

 1:   x = y
 .

Definitions